p, q:. ((p  q)) = ((p) (q))   

latex

ProofTree

Definitions	t  T
Lemmas	bool wf, btrue wf, bfalse wf